1. Field
This disclosure is generally related to electronic design automation. More specifically, this disclosure is related to techniques and systems for simplifying a set of assumptions used during formal circuit verification.
2. Related Art
Describing a circuit using a high-level hardware description language allows hardware engineers to define the circuit's functionality and to optimize the circuit's architecture before converting the high-level description into a detailed physical layout for the circuit.
The goal of formal verification techniques is to prove that the circuit under verification (CUV) will behave as desired during operation. Formal verification techniques typically utilize two types of logical functions: assumptions and assertions. Assumptions are logical functions that are used to model the runtime environment, and assertions are logical functions that define the desired behavior of the CUV. Without assumptions, the CUV is not constrained to legal behavior, and the assertions being verified may be incorrectly falsified.
It is desirable to reduce the amount of time required to formally verify a CUV. Unfortunately, the set of assumptions can be large and complex, and it can sometimes be computationally impractical to perform a formal analysis on the full set of assumptions when attempting to prove or falsify an assertion. Specifically, formal property verification is known to be a PSPACE-hard problem. Hence, a large and complex set of assumptions can disproportionately increase the complexity of the formal verification problem, making it computationally impractical to formally verify a CUV.